(set-logic QF_LIA)
(set-info :source |
Older mathsat benchmarks.  Contact Mathsat group at http://mathsat.itc.it/ for
more information.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun AT0_PROC3_CS () Bool)
(declare-fun AT1_PROC5_X () Int)
(declare-fun AT0_PROC6_SW_B_C_TAU () Bool)
(declare-fun AT1_PROC5_CS () Bool)
(declare-fun AT0_PROC1_X () Int)
(declare-fun AT0_PROC6_C () Bool)
(declare-fun AT0_PROC6_B () Bool)
(declare-fun AT0_PROC6_A () Bool)
(declare-fun AT0_ID0 () Bool)
(declare-fun AT1_PROC2_C () Bool)
(declare-fun AT0_ID1 () Bool)
(declare-fun AT1_PROC2_B () Bool)
(declare-fun AT0_ID2 () Bool)
(declare-fun AT0_PROC6_CS () Bool)
(declare-fun AT1_PROC2_A () Bool)
(declare-fun AT0_ID3 () Bool)
(declare-fun AT0_PROC3_SW_CS_A_TAU () Bool)
(declare-fun AT0_ID4 () Bool)
(declare-fun AT0_ID5 () Bool)
(declare-fun AT1_PROC2_CS () Bool)
(declare-fun AT0_ID6 () Bool)
(declare-fun AT0_PROC4_X () Int)
(declare-fun AT0_PROC3_TAU () Bool)
(declare-fun AT0_PROC6_SW_A_B_TAU () Bool)
(declare-fun AT1_PROC5_C () Bool)
(declare-fun AT0_PROC2_SW_C_B_TAU () Bool)
(declare-fun AT1_PROC5_B () Bool)
(declare-fun AT1_PROC5_A () Bool)
(declare-fun AT0_PROC4_SW_C_B_TAU () Bool)
(declare-fun AT0_PROC1_C () Bool)
(declare-fun AT0_PROC1_B () Bool)
(declare-fun AT0_PROC1_A () Bool)
(declare-fun AT0_PROC6_WAIT () Bool)
(declare-fun AT1_PROC3_X () Int)
(declare-fun AT0_PROC3_WAIT () Bool)
(declare-fun AT0_PROC2_CS () Bool)
(declare-fun AT0_PROC4_C () Bool)
(declare-fun AT0_PROC4_B () Bool)
(declare-fun AT1_ID0 () Bool)
(declare-fun AT1_PROC6_CS () Bool)
(declare-fun AT0_PROC4_A () Bool)
(declare-fun AT1_ID1 () Bool)
(declare-fun AT1_ID2 () Bool)
(declare-fun AT1_ID3 () Bool)
(declare-fun AT1_ID4 () Bool)
(declare-fun AT1_ID5 () Bool)
(declare-fun AT1_ID6 () Bool)
(declare-fun AT0_PROC1_SW_CS_A_TAU () Bool)
(declare-fun AT1_PROC6_X () Int)
(declare-fun AT0_PROC5_SW_C_B_TAU () Bool)
(declare-fun AT0_PROC5_CS () Bool)
(declare-fun AT0_PROC6_SW_C_B_TAU () Bool)
(declare-fun AT0_PROC5_SW_CS_A_TAU () Bool)
(declare-fun AT0_PROC4_TAU () Bool)
(declare-fun AT0_PROC2_X () Int)
(declare-fun AT1_PROC3_CS () Bool)
(declare-fun AT0_PROC4_SW_A_B_TAU () Bool)
(declare-fun AT1_PROC3_C () Bool)
(declare-fun AT1_PROC3_B () Bool)
(declare-fun AT1_PROC3_A () Bool)
(declare-fun AT0_PROC5_X () Int)
(declare-fun AT1_PROC1_X () Int)
(declare-fun AT1_PROC6_C () Bool)
(declare-fun AT1_PROC6_B () Bool)
(declare-fun AT0_PROC6_SW_C_CS_TAU () Bool)
(declare-fun AT1_Z () Int)
(declare-fun AT1_PROC6_A () Bool)
(declare-fun AT0_PROC4_SW_B_C_TAU () Bool)
(declare-fun AT0_PROC2_C () Bool)
(declare-fun AT0_PROC2_SW_C_CS_TAU () Bool)
(declare-fun AT0_PROC2_B () Bool)
(declare-fun AT0_PROC2_A () Bool)
(declare-fun AT0_PROC3_SW_B_C_TAU () Bool)
(declare-fun AT0_PROC1_SW_C_B_TAU () Bool)
(declare-fun AT0_PROC1_CS () Bool)
(declare-fun AT0_PROC5_SW_A_B_TAU () Bool)
(declare-fun AT0_PROC4_WAIT () Bool)
(declare-fun AT0_PROC1_TAU () Bool)
(declare-fun AT0_PROC1_SW_C_CS_TAU () Bool)
(declare-fun AT1_PROC4_X () Int)
(declare-fun AT0_PROC4_SW_CS_A_TAU () Bool)
(declare-fun AT0_PROC1_WAIT () Bool)
(declare-fun AT0_PROC5_TAU () Bool)
(declare-fun AT0_PROC5_SW_C_CS_TAU () Bool)
(declare-fun AT0_PROC5_C () Bool)
(declare-fun AT0_PROC5_B () Bool)
(declare-fun AT0_PROC5_A () Bool)
(declare-fun AT0_PROC4_CS () Bool)
(declare-fun AT1_PROC1_C () Bool)
(declare-fun AT1_PROC1_B () Bool)
(declare-fun AT1_PROC4_CS () Bool)
(declare-fun AT1_PROC1_A () Bool)
(declare-fun AT0_PROC3_SW_A_B_TAU () Bool)
(declare-fun AT0_DELTA () Bool)
(declare-fun AT0_PROC5_SW_B_C_TAU () Bool)
(declare-fun AT0_PROC3_X () Int)
(declare-fun AT0_PROC2_SW_B_C_TAU () Bool)
(declare-fun AT1_PROC4_C () Bool)
(declare-fun AT1_PROC1_CS () Bool)
(declare-fun AT1_PROC4_B () Bool)
(declare-fun AT0_PROC6_SW_CS_A_TAU () Bool)
(declare-fun AT1_PROC4_A () Bool)
(declare-fun AT0_PROC3_SW_C_CS_TAU () Bool)
(declare-fun AT0_PROC1_SW_A_B_TAU () Bool)
(declare-fun AT0_PROC2_SW_CS_A_TAU () Bool)
(declare-fun AT0_PROC6_X () Int)
(declare-fun AT0_PROC2_TAU () Bool)
(declare-fun AT1_PROC2_X () Int)
(declare-fun AT0_PROC4_SW_C_CS_TAU () Bool)
(declare-fun AT0_Z () Int)
(declare-fun AT0_PROC6_TAU () Bool)
(declare-fun AT0_PROC5_WAIT () Bool)
(declare-fun AT0_PROC2_SW_A_B_TAU () Bool)
(declare-fun AT0_PROC3_C () Bool)
(declare-fun AT0_PROC3_B () Bool)
(declare-fun AT0_PROC3_A () Bool)
(declare-fun AT0_PROC3_SW_C_B_TAU () Bool)
(declare-fun AT0_PROC2_WAIT () Bool)
(declare-fun AT0_PROC1_SW_B_C_TAU () Bool)
(assert (let ((?v_0 (not AT0_PROC1_A)) (?v_1 (not AT0_PROC1_B)) (?v_2 (not AT0_PROC1_C)) (?v_3 (not AT0_PROC1_CS)) (?v_4 (not AT1_PROC1_A)) (?v_5 (not AT1_PROC1_B)) (?v_6 (not AT1_PROC1_C)) (?v_7 (not AT1_PROC1_CS)) (?v_8 (not AT0_PROC2_A)) (?v_9 (not AT0_PROC2_B)) (?v_10 (not AT0_PROC2_C)) (?v_11 (not AT0_PROC2_CS)) (?v_12 (not AT1_PROC2_A)) (?v_13 (not AT1_PROC2_B)) (?v_14 (not AT1_PROC2_C)) (?v_15 (not AT1_PROC2_CS)) (?v_16 (not AT0_PROC3_A)) (?v_17 (not AT0_PROC3_B)) (?v_18 (not AT0_PROC3_C)) (?v_19 (not AT0_PROC3_CS)) (?v_20 (not AT1_PROC3_A)) (?v_21 (not AT1_PROC3_B)) (?v_22 (not AT1_PROC3_C)) (?v_23 (not AT1_PROC3_CS)) (?v_24 (not AT0_PROC4_A)) (?v_25 (not AT0_PROC4_B)) (?v_26 (not AT0_PROC4_C)) (?v_27 (not AT0_PROC4_CS)) (?v_28 (not AT1_PROC4_A)) (?v_29 (not AT1_PROC4_B)) (?v_30 (not AT1_PROC4_C)) (?v_31 (not AT1_PROC4_CS)) (?v_32 (not AT0_PROC5_A)) (?v_33 (not AT0_PROC5_B)) (?v_34 (not AT0_PROC5_C)) (?v_35 (not AT0_PROC5_CS)) (?v_36 (not AT1_PROC5_A)) (?v_37 (not AT1_PROC5_B)) (?v_38 (not AT1_PROC5_C)) (?v_39 (not AT1_PROC5_CS)) (?v_40 (not AT0_PROC6_A)) (?v_41 (not AT0_PROC6_B)) (?v_42 (not AT0_PROC6_C)) (?v_43 (not AT0_PROC6_CS)) (?v_44 (not AT1_PROC6_A)) (?v_45 (not AT1_PROC6_B)) (?v_46 (not AT1_PROC6_C)) (?v_47 (not AT1_PROC6_CS)) (?v_48 (= AT0_PROC1_X AT0_Z)) (?v_49 (> AT0_PROC1_X AT0_Z))) (let ((?v_145 (not ?v_48)) (?v_50 (= AT1_PROC1_X AT1_Z)) (?v_51 (> AT1_PROC1_X AT1_Z))) (let ((?v_144 (not ?v_50)) (?v_52 (= AT0_PROC2_X AT0_Z)) (?v_53 (> AT0_PROC2_X AT0_Z))) (let ((?v_150 (not ?v_52)) (?v_54 (= AT1_PROC2_X AT1_Z)) (?v_55 (> AT1_PROC2_X AT1_Z))) (let ((?v_149 (not ?v_54)) (?v_56 (= AT0_PROC3_X AT0_Z)) (?v_57 (> AT0_PROC3_X AT0_Z))) (let ((?v_154 (not ?v_56)) (?v_58 (= AT1_PROC3_X AT1_Z)) (?v_59 (> AT1_PROC3_X AT1_Z))) (let ((?v_153 (not ?v_58)) (?v_60 (= AT0_PROC4_X AT0_Z)) (?v_61 (> AT0_PROC4_X AT0_Z))) (let ((?v_158 (not ?v_60)) (?v_62 (= AT1_PROC4_X AT1_Z)) (?v_63 (> AT1_PROC4_X AT1_Z))) (let ((?v_157 (not ?v_62)) (?v_64 (= AT0_PROC5_X AT0_Z)) (?v_65 (> AT0_PROC5_X AT0_Z))) (let ((?v_162 (not ?v_64)) (?v_66 (= AT1_PROC5_X AT1_Z)) (?v_67 (> AT1_PROC5_X AT1_Z))) (let ((?v_161 (not ?v_66)) (?v_68 (= AT0_PROC6_X AT0_Z)) (?v_69 (> AT0_PROC6_X AT0_Z))) (let ((?v_166 (not ?v_68)) (?v_70 (= AT1_PROC6_X AT1_Z)) (?v_71 (> AT1_PROC6_X AT1_Z))) (let ((?v_165 (not ?v_70)) (?v_77 (- AT0_PROC1_X AT0_Z))) (let ((?v_74 (<= ?v_77 10)) (?v_85 (- AT0_PROC2_X AT0_Z))) (let ((?v_82 (<= ?v_85 10)) (?v_92 (- AT0_PROC3_X AT0_Z))) (let ((?v_89 (<= ?v_92 10)) (?v_99 (- AT0_PROC4_X AT0_Z))) (let ((?v_96 (<= ?v_99 10)) (?v_106 (- AT0_PROC5_X AT0_Z))) (let ((?v_103 (<= ?v_106 10)) (?v_113 (- AT0_PROC6_X AT0_Z))) (let ((?v_110 (<= ?v_113 10)) (?v_72 (not AT0_PROC1_SW_A_B_TAU)) (?v_73 (not AT0_PROC1_SW_B_C_TAU)) (?v_75 (not AT0_PROC1_SW_C_B_TAU)) (?v_76 (not AT0_PROC1_SW_C_CS_TAU)) (?v_116 (= AT1_PROC1_X AT0_PROC1_X)) (?v_78 (not AT0_PROC1_SW_CS_A_TAU)) (?v_79 (= AT1_Z AT0_Z)) (?v_80 (not AT0_PROC2_SW_A_B_TAU)) (?v_81 (not AT0_PROC2_SW_B_C_TAU)) (?v_83 (not AT0_PROC2_SW_C_B_TAU)) (?v_84 (not AT0_PROC2_SW_C_CS_TAU)) (?v_118 (= AT1_PROC2_X AT0_PROC2_X)) (?v_86 (not AT0_PROC2_SW_CS_A_TAU)) (?v_87 (not AT0_PROC3_SW_A_B_TAU)) (?v_88 (not AT0_PROC3_SW_B_C_TAU)) (?v_90 (not AT0_PROC3_SW_C_B_TAU)) (?v_91 (not AT0_PROC3_SW_C_CS_TAU)) (?v_120 (= AT1_PROC3_X AT0_PROC3_X)) (?v_93 (not AT0_PROC3_SW_CS_A_TAU)) (?v_94 (not AT0_PROC4_SW_A_B_TAU)) (?v_95 (not AT0_PROC4_SW_B_C_TAU)) (?v_97 (not AT0_PROC4_SW_C_B_TAU)) (?v_98 (not AT0_PROC4_SW_C_CS_TAU)) (?v_122 (= AT1_PROC4_X AT0_PROC4_X)) (?v_100 (not AT0_PROC4_SW_CS_A_TAU)) (?v_101 (not AT0_PROC5_SW_A_B_TAU)) (?v_102 (not AT0_PROC5_SW_B_C_TAU)) (?v_104 (not AT0_PROC5_SW_C_B_TAU)) (?v_105 (not AT0_PROC5_SW_C_CS_TAU)) (?v_124 (= AT1_PROC5_X AT0_PROC5_X)) (?v_107 (not AT0_PROC5_SW_CS_A_TAU)) (?v_108 (not AT0_PROC6_SW_A_B_TAU)) (?v_109 (not AT0_PROC6_SW_B_C_TAU)) (?v_111 (not AT0_PROC6_SW_C_B_TAU)) (?v_112 (not AT0_PROC6_SW_C_CS_TAU)) (?v_126 (= AT1_PROC6_X AT0_PROC6_X)) (?v_114 (not AT0_PROC6_SW_CS_A_TAU)) (?v_115 (not AT0_PROC1_WAIT)) (?v_128 (not AT0_PROC1_TAU)) (?v_117 (not AT0_PROC2_WAIT)) (?v_129 (not AT0_PROC2_TAU)) (?v_119 (not AT0_PROC3_WAIT)) (?v_131 (not AT0_PROC3_TAU)) (?v_121 (not AT0_PROC4_WAIT)) (?v_132 (not AT0_PROC4_TAU)) (?v_123 (not AT0_PROC5_WAIT)) (?v_133 (not AT0_PROC5_TAU)) (?v_125 (not AT0_PROC6_WAIT)) (?v_134 (not AT0_PROC6_TAU)) (?v_127 (not AT0_DELTA)) (?v_141 (< AT1_Z AT0_Z))) (let ((?v_130 (or ?v_127 ?v_141)) (?v_135 (< AT1_PROC1_X AT0_PROC1_X)) (?v_142 (not ?v_116)) (?v_136 (< AT1_PROC2_X AT0_PROC2_X)) (?v_148 (not ?v_118)) (?v_137 (< AT1_PROC3_X AT0_PROC3_X)) (?v_152 (not ?v_120)) (?v_138 (< AT1_PROC4_X AT0_PROC4_X)) (?v_156 (not ?v_122)) (?v_139 (< AT1_PROC5_X AT0_PROC5_X)) (?v_160 (not ?v_124)) (?v_140 (< AT1_PROC6_X AT0_PROC6_X)) (?v_164 (not ?v_126)) (?v_143 (not ?v_79)) (?v_147 (not ?v_141))) (let ((?v_146 (or ?v_145 ?v_142)) (?v_151 (or ?v_150 ?v_148)) (?v_155 (or ?v_154 ?v_152)) (?v_159 (or ?v_158 ?v_156)) (?v_163 (or ?v_162 ?v_160)) (?v_167 (or ?v_166 ?v_164)) (?v_168 (not AT0_ID0)) (?v_169 (not AT0_ID1)) (?v_170 (not AT0_ID2)) (?v_171 (not AT0_ID3)) (?v_172 (not AT0_ID4)) (?v_173 (not AT0_ID5)) (?v_174 (not AT0_ID6)) (?v_175 (not AT1_ID0)) (?v_176 (not AT1_ID1)) (?v_177 (not AT1_ID2)) (?v_178 (not AT1_ID3)) (?v_179 (not AT1_ID4)) (?v_180 (not AT1_ID5)) (?v_181 (not AT1_ID6)) (?v_182 (- AT1_PROC1_X AT1_Z)) (?v_183 (- AT1_PROC2_X AT1_Z)) (?v_184 (- AT1_PROC3_X AT1_Z)) (?v_185 (- AT1_PROC4_X AT1_Z)) (?v_186 (- AT1_PROC5_X AT1_Z)) (?v_187 (- AT1_PROC6_X AT1_Z))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or ?v_0 ?v_1) (or ?v_0 ?v_2)) (or ?v_0 ?v_3)) (or ?v_1 ?v_2)) (or ?v_1 ?v_3)) (or ?v_2 ?v_3)) (or ?v_4 ?v_5)) (or ?v_4 ?v_6)) (or ?v_4 ?v_7)) (or ?v_5 ?v_6)) (or ?v_5 ?v_7)) (or ?v_6 ?v_7)) (or ?v_8 ?v_9)) (or ?v_8 ?v_10)) (or ?v_8 ?v_11)) (or ?v_9 ?v_10)) (or ?v_9 ?v_11)) (or ?v_10 ?v_11)) (or ?v_12 ?v_13)) (or ?v_12 ?v_14)) (or ?v_12 ?v_15)) (or ?v_13 ?v_14)) (or ?v_13 ?v_15)) (or ?v_14 ?v_15)) (or ?v_16 ?v_17)) (or ?v_16 ?v_18)) (or ?v_16 ?v_19)) (or ?v_17 ?v_18)) (or ?v_17 ?v_19)) (or ?v_18 ?v_19)) (or ?v_20 ?v_21)) (or ?v_20 ?v_22)) (or ?v_20 ?v_23)) (or ?v_21 ?v_22)) (or ?v_21 ?v_23)) (or ?v_22 ?v_23)) (or ?v_24 ?v_25)) (or ?v_24 ?v_26)) (or ?v_24 ?v_27)) (or ?v_25 ?v_26)) (or ?v_25 ?v_27)) (or ?v_26 ?v_27)) (or ?v_28 ?v_29)) (or ?v_28 ?v_30)) (or ?v_28 ?v_31)) (or ?v_29 ?v_30)) (or ?v_29 ?v_31)) (or ?v_30 ?v_31)) (or ?v_32 ?v_33)) (or ?v_32 ?v_34)) (or ?v_32 ?v_35)) (or ?v_33 ?v_34)) (or ?v_33 ?v_35)) (or ?v_34 ?v_35)) (or ?v_36 ?v_37)) (or ?v_36 ?v_38)) (or ?v_36 ?v_39)) (or ?v_37 ?v_38)) (or ?v_37 ?v_39)) (or ?v_38 ?v_39)) (or ?v_40 ?v_41)) (or ?v_40 ?v_42)) (or ?v_40 ?v_43)) (or ?v_41 ?v_42)) (or ?v_41 ?v_43)) (or ?v_42 ?v_43)) (or ?v_44 ?v_45)) (or ?v_44 ?v_46)) (or ?v_44 ?v_47)) (or ?v_45 ?v_46)) (or ?v_45 ?v_47)) (or ?v_46 ?v_47)) (or ?v_48 ?v_49)) (or ?v_145 (not ?v_49))) (or ?v_50 ?v_51)) (or ?v_144 (not ?v_51))) (or ?v_52 ?v_53)) (or ?v_150 (not ?v_53))) (or ?v_54 ?v_55)) (or ?v_149 (not ?v_55))) (or ?v_56 ?v_57)) (or ?v_154 (not ?v_57))) (or ?v_58 ?v_59)) (or ?v_153 (not ?v_59))) (or ?v_60 ?v_61)) (or ?v_158 (not ?v_61))) (or ?v_62 ?v_63)) (or ?v_157 (not ?v_63))) (or ?v_64 ?v_65)) (or ?v_162 (not ?v_65))) (or ?v_66 ?v_67)) (or ?v_161 (not ?v_67))) (or ?v_68 ?v_69)) (or ?v_166 (not ?v_69))) (or ?v_70 ?v_71)) (or ?v_165 (not ?v_71))) (or ?v_1 ?v_74)) (or ?v_5 (<= ?v_182 10))) (or ?v_9 ?v_82)) (or ?v_13 (<= ?v_183 10))) (or ?v_17 ?v_89)) (or ?v_21 (<= ?v_184 10))) (or ?v_25 ?v_96)) (or ?v_29 (<= ?v_185 10))) (or ?v_33 ?v_103)) (or ?v_37 (<= ?v_186 10))) (or ?v_41 ?v_110)) (or ?v_45 (<= ?v_187 10))) (or (or (or (or (or (or AT0_PROC1_WAIT AT0_DELTA) AT0_PROC1_SW_A_B_TAU) AT0_PROC1_SW_B_C_TAU) AT0_PROC1_SW_C_B_TAU) AT0_PROC1_SW_C_CS_TAU) AT0_PROC1_SW_CS_A_TAU)) (or (or (or (or (or (or AT0_PROC2_WAIT AT0_DELTA) AT0_PROC2_SW_A_B_TAU) AT0_PROC2_SW_B_C_TAU) AT0_PROC2_SW_C_B_TAU) AT0_PROC2_SW_C_CS_TAU) AT0_PROC2_SW_CS_A_TAU)) (or (or (or (or (or (or AT0_PROC3_WAIT AT0_DELTA) AT0_PROC3_SW_A_B_TAU) AT0_PROC3_SW_B_C_TAU) AT0_PROC3_SW_C_B_TAU) AT0_PROC3_SW_C_CS_TAU) AT0_PROC3_SW_CS_A_TAU)) (or (or (or (or (or (or AT0_PROC4_WAIT AT0_DELTA) AT0_PROC4_SW_A_B_TAU) AT0_PROC4_SW_B_C_TAU) AT0_PROC4_SW_C_B_TAU) AT0_PROC4_SW_C_CS_TAU) AT0_PROC4_SW_CS_A_TAU)) (or (or (or (or (or (or AT0_PROC5_WAIT AT0_DELTA) AT0_PROC5_SW_A_B_TAU) AT0_PROC5_SW_B_C_TAU) AT0_PROC5_SW_C_B_TAU) AT0_PROC5_SW_C_CS_TAU) AT0_PROC5_SW_CS_A_TAU)) (or (or (or (or (or (or AT0_PROC6_WAIT AT0_DELTA) AT0_PROC6_SW_A_B_TAU) AT0_PROC6_SW_B_C_TAU) AT0_PROC6_SW_C_B_TAU) AT0_PROC6_SW_C_CS_TAU) AT0_PROC6_SW_CS_A_TAU)) (or ?v_72 AT0_PROC1_A)) (or ?v_72 AT0_PROC1_TAU)) (or ?v_72 AT1_PROC1_B)) (or ?v_72 ?v_50)) (or ?v_73 AT0_PROC1_B)) (or ?v_73 AT0_PROC1_TAU)) (or ?v_73 AT1_PROC1_C)) (or ?v_73 ?v_74)) (or ?v_73 ?v_50)) (or ?v_75 AT0_PROC1_C)) (or ?v_75 AT0_PROC1_TAU)) (or ?v_75 AT1_PROC1_B)) (or ?v_75 ?v_50)) (or ?v_76 AT0_PROC1_C)) (or ?v_76 AT0_PROC1_TAU)) (or ?v_76 AT1_PROC1_CS)) (or ?v_76 (> ?v_77 10))) (or ?v_76 ?v_116)) (or ?v_78 AT0_PROC1_CS)) (or ?v_78 AT0_PROC1_TAU)) (or ?v_78 AT1_PROC1_A)) (or ?v_78 ?v_50)) (or ?v_72 ?v_79)) (or ?v_73 ?v_79)) (or ?v_75 ?v_79)) (or ?v_76 ?v_79)) (or ?v_78 ?v_79)) (or ?v_80 AT0_PROC2_A)) (or ?v_80 AT0_PROC2_TAU)) (or ?v_80 AT1_PROC2_B)) (or ?v_80 ?v_54)) (or ?v_81 AT0_PROC2_B)) (or ?v_81 AT0_PROC2_TAU)) (or ?v_81 AT1_PROC2_C)) (or ?v_81 ?v_82)) (or ?v_81 ?v_54)) (or ?v_83 AT0_PROC2_C)) (or ?v_83 AT0_PROC2_TAU)) (or ?v_83 AT1_PROC2_B)) (or ?v_83 ?v_54)) (or ?v_84 AT0_PROC2_C)) (or ?v_84 AT0_PROC2_TAU)) (or ?v_84 AT1_PROC2_CS)) (or ?v_84 (> ?v_85 10))) (or ?v_84 ?v_118)) (or ?v_86 AT0_PROC2_CS)) (or ?v_86 AT0_PROC2_TAU)) (or ?v_86 AT1_PROC2_A)) (or ?v_86 ?v_54)) (or ?v_80 ?v_79)) (or ?v_81 ?v_79)) (or ?v_83 ?v_79)) (or ?v_84 ?v_79)) (or ?v_86 ?v_79)) (or ?v_87 AT0_PROC3_A)) (or ?v_87 AT0_PROC3_TAU)) (or ?v_87 AT1_PROC3_B)) (or ?v_87 ?v_58)) (or ?v_88 AT0_PROC3_B)) (or ?v_88 AT0_PROC3_TAU)) (or ?v_88 AT1_PROC3_C)) (or ?v_88 ?v_89)) (or ?v_88 ?v_58)) (or ?v_90 AT0_PROC3_C)) (or ?v_90 AT0_PROC3_TAU)) (or ?v_90 AT1_PROC3_B)) (or ?v_90 ?v_58)) (or ?v_91 AT0_PROC3_C)) (or ?v_91 AT0_PROC3_TAU)) (or ?v_91 AT1_PROC3_CS)) (or ?v_91 (> ?v_92 10))) (or ?v_91 ?v_120)) (or ?v_93 AT0_PROC3_CS)) (or ?v_93 AT0_PROC3_TAU)) (or ?v_93 AT1_PROC3_A)) (or ?v_93 ?v_58)) (or ?v_87 ?v_79)) (or ?v_88 ?v_79)) (or ?v_90 ?v_79)) (or ?v_91 ?v_79)) (or ?v_93 ?v_79)) (or ?v_94 AT0_PROC4_A)) (or ?v_94 AT0_PROC4_TAU)) (or ?v_94 AT1_PROC4_B)) (or ?v_94 ?v_62)) (or ?v_95 AT0_PROC4_B)) (or ?v_95 AT0_PROC4_TAU)) (or ?v_95 AT1_PROC4_C)) (or ?v_95 ?v_96)) (or ?v_95 ?v_62)) (or ?v_97 AT0_PROC4_C)) (or ?v_97 AT0_PROC4_TAU)) (or ?v_97 AT1_PROC4_B)) (or ?v_97 ?v_62)) (or ?v_98 AT0_PROC4_C)) (or ?v_98 AT0_PROC4_TAU)) (or ?v_98 AT1_PROC4_CS)) (or ?v_98 (> ?v_99 10))) (or ?v_98 ?v_122)) (or ?v_100 AT0_PROC4_CS)) (or ?v_100 AT0_PROC4_TAU)) (or ?v_100 AT1_PROC4_A)) (or ?v_100 ?v_62)) (or ?v_94 ?v_79)) (or ?v_95 ?v_79)) (or ?v_97 ?v_79)) (or ?v_98 ?v_79)) (or ?v_100 ?v_79)) (or ?v_101 AT0_PROC5_A)) (or ?v_101 AT0_PROC5_TAU)) (or ?v_101 AT1_PROC5_B)) (or ?v_101 ?v_66)) (or ?v_102 AT0_PROC5_B)) (or ?v_102 AT0_PROC5_TAU)) (or ?v_102 AT1_PROC5_C)) (or ?v_102 ?v_103)) (or ?v_102 ?v_66)) (or ?v_104 AT0_PROC5_C)) (or ?v_104 AT0_PROC5_TAU)) (or ?v_104 AT1_PROC5_B)) (or ?v_104 ?v_66)) (or ?v_105 AT0_PROC5_C)) (or ?v_105 AT0_PROC5_TAU)) (or ?v_105 AT1_PROC5_CS)) (or ?v_105 (> ?v_106 10))) (or ?v_105 ?v_124)) (or ?v_107 AT0_PROC5_CS)) (or ?v_107 AT0_PROC5_TAU)) (or ?v_107 AT1_PROC5_A)) (or ?v_107 ?v_66)) (or ?v_101 ?v_79)) (or ?v_102 ?v_79)) (or ?v_104 ?v_79)) (or ?v_105 ?v_79)) (or ?v_107 ?v_79)) (or ?v_108 AT0_PROC6_A)) (or ?v_108 AT0_PROC6_TAU)) (or ?v_108 AT1_PROC6_B)) (or ?v_108 ?v_70)) (or ?v_109 AT0_PROC6_B)) (or ?v_109 AT0_PROC6_TAU)) (or ?v_109 AT1_PROC6_C)) (or ?v_109 ?v_110)) (or ?v_109 ?v_70)) (or ?v_111 AT0_PROC6_C)) (or ?v_111 AT0_PROC6_TAU)) (or ?v_111 AT1_PROC6_B)) (or ?v_111 ?v_70)) (or ?v_112 AT0_PROC6_C)) (or ?v_112 AT0_PROC6_TAU)) (or ?v_112 AT1_PROC6_CS)) (or ?v_112 (> ?v_113 10))) (or ?v_112 ?v_126)) (or ?v_114 AT0_PROC6_CS)) (or ?v_114 AT0_PROC6_TAU)) (or ?v_114 AT1_PROC6_A)) (or ?v_114 ?v_70)) (or ?v_108 ?v_79)) (or ?v_109 ?v_79)) (or ?v_111 ?v_79)) (or ?v_112 ?v_79)) (or ?v_114 ?v_79)) (or (or ?v_115 ?v_0) AT1_PROC1_A)) (or (or ?v_115 AT0_PROC1_A) ?v_4)) (or (or ?v_115 ?v_1) AT1_PROC1_B)) (or (or ?v_115 AT0_PROC1_B) ?v_5)) (or (or ?v_115 ?v_2) AT1_PROC1_C)) (or (or ?v_115 AT0_PROC1_C) ?v_6)) (or (or ?v_115 ?v_3) AT1_PROC1_CS)) (or (or ?v_115 AT0_PROC1_CS) ?v_7)) (or ?v_115 ?v_128)) (or ?v_115 ?v_116)) (or ?v_115 ?v_79)) (or (or ?v_117 ?v_8) AT1_PROC2_A)) (or (or ?v_117 AT0_PROC2_A) ?v_12)) (or (or ?v_117 ?v_9) AT1_PROC2_B)) (or (or ?v_117 AT0_PROC2_B) ?v_13)) (or (or ?v_117 ?v_10) AT1_PROC2_C)) (or (or ?v_117 AT0_PROC2_C) ?v_14)) (or (or ?v_117 ?v_11) AT1_PROC2_CS)) (or (or ?v_117 AT0_PROC2_CS) ?v_15)) (or ?v_117 ?v_129)) (or ?v_117 ?v_118)) (or ?v_117 ?v_79)) (or (or ?v_119 ?v_16) AT1_PROC3_A)) (or (or ?v_119 AT0_PROC3_A) ?v_20)) (or (or ?v_119 ?v_17) AT1_PROC3_B)) (or (or ?v_119 AT0_PROC3_B) ?v_21)) (or (or ?v_119 ?v_18) AT1_PROC3_C)) (or (or ?v_119 AT0_PROC3_C) ?v_22)) (or (or ?v_119 ?v_19) AT1_PROC3_CS)) (or (or ?v_119 AT0_PROC3_CS) ?v_23)) (or ?v_119 ?v_131)) (or ?v_119 ?v_120)) (or ?v_119 ?v_79)) (or (or ?v_121 ?v_24) AT1_PROC4_A)) (or (or ?v_121 AT0_PROC4_A) ?v_28)) (or (or ?v_121 ?v_25) AT1_PROC4_B)) (or (or ?v_121 AT0_PROC4_B) ?v_29)) (or (or ?v_121 ?v_26) AT1_PROC4_C)) (or (or ?v_121 AT0_PROC4_C) ?v_30)) (or (or ?v_121 ?v_27) AT1_PROC4_CS)) (or (or ?v_121 AT0_PROC4_CS) ?v_31)) (or ?v_121 ?v_132)) (or ?v_121 ?v_122)) (or ?v_121 ?v_79)) (or (or ?v_123 ?v_32) AT1_PROC5_A)) (or (or ?v_123 AT0_PROC5_A) ?v_36)) (or (or ?v_123 ?v_33) AT1_PROC5_B)) (or (or ?v_123 AT0_PROC5_B) ?v_37)) (or (or ?v_123 ?v_34) AT1_PROC5_C)) (or (or ?v_123 AT0_PROC5_C) ?v_38)) (or (or ?v_123 ?v_35) AT1_PROC5_CS)) (or (or ?v_123 AT0_PROC5_CS) ?v_39)) (or ?v_123 ?v_133)) (or ?v_123 ?v_124)) (or ?v_123 ?v_79)) (or (or ?v_125 ?v_40) AT1_PROC6_A)) (or (or ?v_125 AT0_PROC6_A) ?v_44)) (or (or ?v_125 ?v_41) AT1_PROC6_B)) (or (or ?v_125 AT0_PROC6_B) ?v_45)) (or (or ?v_125 ?v_42) AT1_PROC6_C)) (or (or ?v_125 AT0_PROC6_C) ?v_46)) (or (or ?v_125 ?v_43) AT1_PROC6_CS)) (or (or ?v_125 AT0_PROC6_CS) ?v_47)) (or ?v_125 ?v_134)) (or ?v_125 ?v_126)) (or ?v_125 ?v_79)) (or (or ?v_127 ?v_0) AT1_PROC1_A)) (or (or ?v_127 AT0_PROC1_A) ?v_4)) (or (or ?v_127 ?v_1) AT1_PROC1_B)) (or (or ?v_127 AT0_PROC1_B) ?v_5)) (or (or ?v_127 ?v_2) AT1_PROC1_C)) (or (or ?v_127 AT0_PROC1_C) ?v_6)) (or (or ?v_127 ?v_3) AT1_PROC1_CS)) (or (or ?v_127 AT0_PROC1_CS) ?v_7)) (or ?v_127 ?v_116)) (or ?v_127 ?v_128)) ?v_130) (or (or ?v_127 ?v_8) AT1_PROC2_A)) (or (or ?v_127 AT0_PROC2_A) ?v_12)) (or (or ?v_127 ?v_9) AT1_PROC2_B)) (or (or ?v_127 AT0_PROC2_B) ?v_13)) (or (or ?v_127 ?v_10) AT1_PROC2_C)) (or (or ?v_127 AT0_PROC2_C) ?v_14)) (or (or ?v_127 ?v_11) AT1_PROC2_CS)) (or (or ?v_127 AT0_PROC2_CS) ?v_15)) (or ?v_127 ?v_118)) (or ?v_127 ?v_129)) ?v_130) (or (or ?v_127 ?v_16) AT1_PROC3_A)) (or (or ?v_127 AT0_PROC3_A) ?v_20)) (or (or ?v_127 ?v_17) AT1_PROC3_B)) (or (or ?v_127 AT0_PROC3_B) ?v_21)) (or (or ?v_127 ?v_18) AT1_PROC3_C)) (or (or ?v_127 AT0_PROC3_C) ?v_22)) (or (or ?v_127 ?v_19) AT1_PROC3_CS)) (or (or ?v_127 AT0_PROC3_CS) ?v_23)) (or ?v_127 ?v_120)) (or ?v_127 ?v_131)) ?v_130) (or (or ?v_127 ?v_24) AT1_PROC4_A)) (or (or ?v_127 AT0_PROC4_A) ?v_28)) (or (or ?v_127 ?v_25) AT1_PROC4_B)) (or (or ?v_127 AT0_PROC4_B) ?v_29)) (or (or ?v_127 ?v_26) AT1_PROC4_C)) (or (or ?v_127 AT0_PROC4_C) ?v_30)) (or (or ?v_127 ?v_27) AT1_PROC4_CS)) (or (or ?v_127 AT0_PROC4_CS) ?v_31)) (or ?v_127 ?v_122)) (or ?v_127 ?v_132)) ?v_130) (or (or ?v_127 ?v_32) AT1_PROC5_A)) (or (or ?v_127 AT0_PROC5_A) ?v_36)) (or (or ?v_127 ?v_33) AT1_PROC5_B)) (or (or ?v_127 AT0_PROC5_B) ?v_37)) (or (or ?v_127 ?v_34) AT1_PROC5_C)) (or (or ?v_127 AT0_PROC5_C) ?v_38)) (or (or ?v_127 ?v_35) AT1_PROC5_CS)) (or (or ?v_127 AT0_PROC5_CS) ?v_39)) (or ?v_127 ?v_124)) (or ?v_127 ?v_133)) ?v_130) (or (or ?v_127 ?v_40) AT1_PROC6_A)) (or (or ?v_127 AT0_PROC6_A) ?v_44)) (or (or ?v_127 ?v_41) AT1_PROC6_B)) (or (or ?v_127 AT0_PROC6_B) ?v_45)) (or (or ?v_127 ?v_42) AT1_PROC6_C)) (or (or ?v_127 AT0_PROC6_C) ?v_46)) (or (or ?v_127 ?v_43) AT1_PROC6_CS)) (or (or ?v_127 AT0_PROC6_CS) ?v_47)) (or ?v_127 ?v_126)) (or ?v_127 ?v_134)) ?v_130) (or ?v_116 ?v_135)) (or ?v_142 (not ?v_135))) (or ?v_118 ?v_136)) (or ?v_148 (not ?v_136))) (or ?v_120 ?v_137)) (or ?v_152 (not ?v_137))) (or ?v_122 ?v_138)) (or ?v_156 (not ?v_138))) (or ?v_124 ?v_139)) (or ?v_160 (not ?v_139))) (or ?v_126 ?v_140)) (or ?v_164 (not ?v_140))) (or ?v_79 ?v_141)) (or ?v_143 ?v_147)) (or (or (or ?v_48 ?v_142) ?v_143) ?v_144)) (or (or (or ?v_145 ?v_116) ?v_143) ?v_144)) (or (or ?v_146 ?v_79) ?v_144)) (or (or ?v_146 ?v_143) ?v_50)) (or (or (or (not (< AT0_Z AT0_PROC1_X)) ?v_142) ?v_147) (< AT1_Z AT1_PROC1_X))) (or (or (or ?v_52 ?v_148) ?v_143) ?v_149)) (or (or (or ?v_150 ?v_118) ?v_143) ?v_149)) (or (or ?v_151 ?v_79) ?v_149)) (or (or ?v_151 ?v_143) ?v_54)) (or (or (or (not (< AT0_Z AT0_PROC2_X)) ?v_148) ?v_147) (< AT1_Z AT1_PROC2_X))) (or (or (or ?v_56 ?v_152) ?v_143) ?v_153)) (or (or (or ?v_154 ?v_120) ?v_143) ?v_153)) (or (or ?v_155 ?v_79) ?v_153)) (or (or ?v_155 ?v_143) ?v_58)) (or (or (or (not (< AT0_Z AT0_PROC3_X)) ?v_152) ?v_147) (< AT1_Z AT1_PROC3_X))) (or (or (or ?v_60 ?v_156) ?v_143) ?v_157)) (or (or (or ?v_158 ?v_122) ?v_143) ?v_157)) (or (or ?v_159 ?v_79) ?v_157)) (or (or ?v_159 ?v_143) ?v_62)) (or (or (or (not (< AT0_Z AT0_PROC4_X)) ?v_156) ?v_147) (< AT1_Z AT1_PROC4_X))) (or (or (or ?v_64 ?v_160) ?v_143) ?v_161)) (or (or (or ?v_162 ?v_124) ?v_143) ?v_161)) (or (or ?v_163 ?v_79) ?v_161)) (or (or ?v_163 ?v_143) ?v_66)) (or (or (or (not (< AT0_Z AT0_PROC5_X)) ?v_160) ?v_147) (< AT1_Z AT1_PROC5_X))) (or (or (or ?v_68 ?v_164) ?v_143) ?v_165)) (or (or (or ?v_166 ?v_126) ?v_143) ?v_165)) (or (or ?v_167 ?v_79) ?v_165)) (or (or ?v_167 ?v_143) ?v_70)) (or (or (or (not (< AT0_Z AT0_PROC6_X)) ?v_164) ?v_147) (< AT1_Z AT1_PROC6_X))) AT0_PROC1_A) AT0_PROC2_A) AT0_PROC3_A) AT0_PROC4_A) AT0_PROC5_A) AT0_PROC6_A) ?v_48) ?v_52) ?v_56) ?v_60) ?v_64) ?v_68) AT0_ID0) (or (or (or (or (or ?v_115 ?v_117) ?v_119) ?v_121) ?v_123) ?v_125)) (or ?v_168 ?v_169)) (or ?v_168 ?v_170)) (or ?v_168 ?v_171)) (or ?v_168 ?v_172)) (or ?v_168 ?v_173)) (or ?v_168 ?v_174)) (or ?v_169 ?v_170)) (or ?v_169 ?v_171)) (or ?v_169 ?v_172)) (or ?v_169 ?v_173)) (or ?v_169 ?v_174)) (or ?v_170 ?v_171)) (or ?v_170 ?v_172)) (or ?v_170 ?v_173)) (or ?v_170 ?v_174)) (or ?v_171 ?v_172)) (or ?v_171 ?v_173)) (or ?v_171 ?v_174)) (or ?v_172 ?v_173)) (or ?v_172 ?v_174)) (or ?v_173 ?v_174)) (or ?v_175 ?v_176)) (or ?v_175 ?v_177)) (or ?v_175 ?v_178)) (or ?v_175 ?v_179)) (or ?v_175 ?v_180)) (or ?v_175 ?v_181)) (or ?v_176 ?v_177)) (or ?v_176 ?v_178)) (or ?v_176 ?v_179)) (or ?v_176 ?v_180)) (or ?v_176 ?v_181)) (or ?v_177 ?v_178)) (or ?v_177 ?v_179)) (or ?v_177 ?v_180)) (or ?v_177 ?v_181)) (or ?v_178 ?v_179)) (or ?v_178 ?v_180)) (or ?v_178 ?v_181)) (or ?v_179 ?v_180)) (or ?v_179 ?v_181)) (or ?v_180 ?v_181)) (or ?v_72 AT0_ID0)) (or ?v_72 AT1_ID0)) (or ?v_73 AT1_ID1)) (or ?v_75 AT0_ID0)) (or ?v_75 AT1_ID0)) (or ?v_76 AT0_ID1)) (or ?v_76 AT1_ID1)) (or ?v_78 AT1_ID0)) (or (or ?v_127 ?v_169) AT1_ID1)) (or ?v_80 AT0_ID0)) (or ?v_80 AT1_ID0)) (or ?v_81 AT1_ID2)) (or ?v_83 AT0_ID0)) (or ?v_83 AT1_ID0)) (or ?v_84 AT0_ID2)) (or ?v_84 AT1_ID2)) (or ?v_86 AT1_ID0)) (or (or ?v_127 ?v_170) AT1_ID2)) (or ?v_87 AT0_ID0)) (or ?v_87 AT1_ID0)) (or ?v_88 AT1_ID3)) (or ?v_90 AT0_ID0)) (or ?v_90 AT1_ID0)) (or ?v_91 AT0_ID3)) (or ?v_91 AT1_ID3)) (or ?v_93 AT1_ID0)) (or (or ?v_127 ?v_171) AT1_ID3)) (or ?v_94 AT0_ID0)) (or ?v_94 AT1_ID0)) (or ?v_95 AT1_ID4)) (or ?v_97 AT0_ID0)) (or ?v_97 AT1_ID0)) (or ?v_98 AT0_ID4)) (or ?v_98 AT1_ID4)) (or ?v_100 AT1_ID0)) (or (or ?v_127 ?v_172) AT1_ID4)) (or ?v_101 AT0_ID0)) (or ?v_101 AT1_ID0)) (or ?v_102 AT1_ID5)) (or ?v_104 AT0_ID0)) (or ?v_104 AT1_ID0)) (or ?v_105 AT0_ID5)) (or ?v_105 AT1_ID5)) (or ?v_107 AT1_ID0)) (or (or ?v_127 ?v_173) AT1_ID5)) (or ?v_108 AT0_ID0)) (or ?v_108 AT1_ID0)) (or ?v_109 AT1_ID6)) (or ?v_111 AT0_ID0)) (or ?v_111 AT1_ID0)) (or ?v_112 AT0_ID6)) (or ?v_112 AT1_ID6)) (or ?v_114 AT1_ID0)) (or (or ?v_127 ?v_174) AT1_ID6)) (or (or ?v_127 ?v_168) AT1_ID0)) (or ?v_4 AT1_PROC1_A)) (or AT1_PROC1_A ?v_4)) (or ?v_5 AT1_PROC1_B)) (or AT1_PROC1_B ?v_5)) (or ?v_6 AT1_PROC1_C)) (or AT1_PROC1_C ?v_6)) (or ?v_7 AT1_PROC1_CS)) (or AT1_PROC1_CS ?v_7)) (or ?v_176 AT1_ID1)) (or AT1_ID1 ?v_176)) (= ?v_182 ?v_182)) (or ?v_12 AT1_PROC2_A)) (or AT1_PROC2_A ?v_12)) (or ?v_13 AT1_PROC2_B)) (or AT1_PROC2_B ?v_13)) (or ?v_14 AT1_PROC2_C)) (or AT1_PROC2_C ?v_14)) (or ?v_15 AT1_PROC2_CS)) (or AT1_PROC2_CS ?v_15)) (or ?v_177 AT1_ID2)) (or AT1_ID2 ?v_177)) (= ?v_183 ?v_183)) (or ?v_20 AT1_PROC3_A)) (or AT1_PROC3_A ?v_20)) (or ?v_21 AT1_PROC3_B)) (or AT1_PROC3_B ?v_21)) (or ?v_22 AT1_PROC3_C)) (or AT1_PROC3_C ?v_22)) (or ?v_23 AT1_PROC3_CS)) (or AT1_PROC3_CS ?v_23)) (or ?v_178 AT1_ID3)) (or AT1_ID3 ?v_178)) (= ?v_184 ?v_184)) (or ?v_28 AT1_PROC4_A)) (or AT1_PROC4_A ?v_28)) (or ?v_29 AT1_PROC4_B)) (or AT1_PROC4_B ?v_29)) (or ?v_30 AT1_PROC4_C)) (or AT1_PROC4_C ?v_30)) (or ?v_31 AT1_PROC4_CS)) (or AT1_PROC4_CS ?v_31)) (or ?v_179 AT1_ID4)) (or AT1_ID4 ?v_179)) (= ?v_185 ?v_185)) (or ?v_36 AT1_PROC5_A)) (or AT1_PROC5_A ?v_36)) (or ?v_37 AT1_PROC5_B)) (or AT1_PROC5_B ?v_37)) (or ?v_38 AT1_PROC5_C)) (or AT1_PROC5_C ?v_38)) (or ?v_39 AT1_PROC5_CS)) (or AT1_PROC5_CS ?v_39)) (or ?v_180 AT1_ID5)) (or AT1_ID5 ?v_180)) (= ?v_186 ?v_186)) (or ?v_44 AT1_PROC6_A)) (or AT1_PROC6_A ?v_44)) (or ?v_45 AT1_PROC6_B)) (or AT1_PROC6_B ?v_45)) (or ?v_46 AT1_PROC6_C)) (or AT1_PROC6_C ?v_46)) (or ?v_47 AT1_PROC6_CS)) (or AT1_PROC6_CS ?v_47)) (or ?v_181 AT1_ID6)) (or AT1_ID6 ?v_181)) (= ?v_187 ?v_187)) AT1_PROC1_B) ?v_7)))))))))))))))))))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
